/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ ∧Abstract Syntax and Semantics of Programs with go to␈↓

␈↓ α∧␈↓α␈↓ ∧wby John McCarthy, Stanford University

␈↓ α∧␈↓␈↓ αTThe␈α∞object␈α∂of␈α∞this␈α∂note␈α∞is␈α∞to␈α∂give␈α∞an␈α∂example␈α∞of␈α∞the␈α∂abstract␈α∞syntax␈α∂and␈α∞semantics␈α∂of␈α∞a
␈↓ α∧␈↓programming␈α∞language␈α∞(call␈α∞it␈α∂␈↓↓F1)␈α∞␈↓␈α∞which␈α∞is␈α∞far␈α∂from␈α∞context␈α∞free.␈α∞ We␈α∞choose␈α∂programs␈α∞with
␈↓ α∧␈↓assignments,␈α
conditionals␈α
and␈α
␈↓αgo to␈↓s,␈α
because␈α
we␈α
want␈α
our␈α
syntax␈α
to␈α
express␈α
the␈α
fact␈α
that␈α
for␈α
every
␈↓ α∧␈↓␈↓αgo to␈↓, the corresponding label must exist, and no label should occur more than once.

␈↓ α∧␈↓␈↓ αTThe␈α
simplest␈α
formulation␈α
supposes␈α
that␈α
each␈αassignment␈α
statement␈α
has␈α
both␈α
a␈α
label␈α
and␈αa
␈↓ α∧␈↓␈↓αgo to␈↓.␈α∞ We␈α∂identify␈α∞a␈α∂statement␈α∞with␈α∂the␈α∞unit␈α∞set␈α∂containing␈α∞just␈α∂that␈α∞statement.␈α∂ Programs␈α∞are
␈↓ α∧␈↓constructed in two ways.

␈↓ α∧␈↓␈↓ αT1. An elementary statement ␈↓↓elem(l1,p,f,l2,l3)␈↓ is a program.  Its intuitive interpretation is

␈↓ α∧␈↓␈↓↓l1:␈↓ β∀␈↓αif␈↓↓ p(␈↓	x␈↓↓) ␈↓αthen␈↓↓ ␈↓αbegin␈↓↓ ␈↓	x␈↓↓ ← f(␈↓	x␈↓↓); ␈↓αgo to␈↓↓ l2 ␈↓αend␈↓↓ ␈↓αelse␈↓↓ ␈↓αgo to␈↓↓ l3;␈↓

␈↓ α∧␈↓Here␈α␈↓	x␈↓␈αis␈αa␈αstate␈αvector,␈α␈↓↓p␈↓␈αis␈αa␈αpredicate␈αof␈αstate␈αvectors,␈αand␈α␈↓↓f␈↓␈αis␈αa␈αfunction␈αfrom␈αstate␈αvectors␈αto
␈↓ α∧␈↓state␈α∂vectors.␈α∂ Putting␈α∞labels,␈α∂a␈α∂conditional␈α∂␈↓αgo to␈↓␈α∞and␈α∂an␈α∂assignment␈α∞all␈α∂into␈α∂every␈α∂statement␈α∞is
␈↓ α∧␈↓merely␈α
a␈α
convenience␈α
in␈α
giving␈α
the␈α
theory.␈α∞ The␈α
more␈α
usual␈α
ways␈α
of␈α
writing␈α
such␈α∞programs␈α
are
␈↓ α∧␈↓obtainable by specializing this general form.

␈↓ α∧␈↓␈↓ αT2.␈α∂If␈α⊂␈↓↓u␈↓␈α∂and␈α⊂␈↓↓v␈↓␈α∂are␈α⊂programs,␈α∂so␈α∂is␈α⊂␈↓↓u ∪ v␈↓.␈α∂ We␈α⊂can␈α∂take␈α⊂union␈α∂rather␈α⊂than␈α∂concatenation,
␈↓ α∧␈↓because all statements have labels.

␈↓ α∧␈↓Well-formedness

␈↓ α∧␈↓␈↓ αTNot␈α
every␈α
program␈α
is␈α
well-formed,␈αbecause␈α
there␈α
may␈α
be␈α
incompatible␈α
labels.␈α Therefore,␈α
we
␈↓ α∧␈↓have␈α∀a␈α∀predicate␈α∀␈↓↓ok(u)␈↓␈α∪and␈α∀two␈α∀auxiliary␈α∀functions␈α∪␈↓↓labels(u)␈↓␈α∀and␈α∀␈↓↓outlabels(u)␈↓␈α∀satisfying␈α∪the
␈↓ α∧␈↓following syntactic axioms in which free variables are assumed universally quantified.

␈↓ α∧␈↓1. ␈↓↓ok elem(l1,p,f,l2,l3)

␈↓ α∧␈↓↓2. labels elem(l1,p,f,l2,l3) = {l1}

␈↓ α∧␈↓↓3. outlabels elem(l1,p,f,l2,l3) = {l2,l3}

␈↓ α∧␈↓↓4. ok (u ∪ v) ≡ ok u ∧ ok v ∧ labels(u) ∩ labels(v) = {}

␈↓ α∧␈↓↓5. labels(u ∪ v) = labels(u) ∪ labels(v)

␈↓ α∧␈↓↓6. outlabels(u ∪ v) = (outlabels(u) ∪ outlabels(v)) \ (labels(u) ∪ labels(v))␈↓

␈↓ α∧␈↓␈↓ αTA␈α
program␈α
␈↓↓u␈↓␈αmay␈α
be␈α
called␈α
complete␈αif␈α
␈↓↓outlabels(u)␈α
={done}␈↓,␈αwhere␈α
␈↓↓done␈↓␈α
is␈α
a␈αdistinguished
␈↓ α∧␈↓label denoting the end of the program.

␈↓ α∧␈↓Semantics

␈↓ α∧␈↓␈↓ αTThe␈α∪semantics␈α∩of␈α∪␈↓↓F1␈↓␈α∩is␈α∪given␈α∩by␈α∪a␈α∩predicate␈α∪␈↓↓whither␈↓␈α∩and␈α∪a␈α∩partial␈α∪function␈α∩␈↓↓outome.␈↓
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓␈↓↓whither(l1,u,l2,␈↓	x␈↓↓)␈↓␈αis␈αtrue␈αif␈αentering␈αthe␈αprogram␈α␈↓↓u␈↓␈αat␈αlabel␈α␈↓↓l1␈↓␈αin␈αstate␈α␈↓	x␈↓␈αwill␈αresult␈αin␈αan␈αexit␈αat
␈↓ α∧␈↓␈↓↓l2.␈↓␈α
␈↓↓outcome(l1,u,␈↓	x␈↓↓)␈↓␈α
is␈α
the␈α
state␈α
that␈α
results␈α
when␈α
the␈α
program␈α
␈↓↓u␈↓␈α
is␈α
entered␈α
at␈α
label␈α
␈↓↓l1␈↓␈α
while␈αin␈α
state
␈↓ α∧␈↓␈↓	x␈↓.  ␈↓↓whither␈↓ and ␈↓↓outcome␈↓ are easily given for elementary programs.  Namely

␈↓ α∧␈↓␈↓ αT␈↓↓whither(l1,elem(l1',p,f,l2',l3'),l2,␈↓	x␈↓↓) ≡ l1 = l1' ∧ (␈↓αif␈↓↓ p(␈↓	x␈↓↓) ␈↓αthen␈↓↓ l2 = l2' ␈↓αelse␈↓↓ l2 = l3')␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓outcome(l1,elem(l1',p,f,l2',l3'),␈↓	x␈↓↓) = ␈↓αif␈↓↓ l1 = l1' ␈↓αthen␈↓↓ (␈↓αif␈↓↓ p(␈↓	x␈↓↓) ␈↓αthen␈↓↓ f(␈↓	x␈↓↓) ␈↓αelse␈↓↓ ␈↓	x␈↓↓)␈↓.

␈↓ α∧␈↓We consider ␈↓↓outcome(l1,elem(l1',p,f,l2',l3'),␈↓	x␈↓↓)␈↓ undefined if ␈↓↓l1␈↓ and ␈↓↓l1'␈↓ are not equal.

␈↓ α∧␈↓␈↓ αTNext␈α∪we␈α∪need␈α∩to␈α∪define␈α∪␈↓↓whither(l1,u ∪ v,l2,␈↓	x␈↓↓)␈↓␈α∩and␈α∪␈↓↓outcome(l1,u ∪ v,␈↓	x␈↓↓)␈↓.␈α∪ This␈α∪is␈α∩more
␈↓ α∧␈↓difficult,␈α
because␈α
control␈αmay␈α
go␈α
back␈αand␈α
forth␈α
between␈αthe␈α
statements␈α
of␈α␈↓↓u␈↓␈α
and␈α
the␈αstatements␈α
of
␈↓ α∧␈↓␈↓↓v␈↓ an arbitrary number of times, so we have a complicated recursion.

␈↓ α∧␈↓␈↓↓whither(l1,u ∪ v,l2,␈↓	x␈↓↓) ≡
␈↓ α∧␈↓↓␈↓ βd[l1 ε labels(u) ∧
␈↓ α∧␈↓↓␈↓ ∧4whither(l1,u,l2,␈↓	x␈↓↓) ∨
␈↓ α∧␈↓↓␈↓ ¬∧∃l.l ≠ l2 ∧ whither(l1,u,l,␈↓	x␈↓↓)
␈↓ α∧␈↓↓␈↓ ¬T∧ whither(l,u ∪ v,l2,outcome(l1,u,␈↓	x␈↓↓))]]
␈↓ α∧␈↓↓␈↓ βd∨ [l1 ε labels(v) ∧
␈↓ α∧␈↓↓␈↓ ∧4whither(l1,v,l2,␈↓	x␈↓↓) ∨
␈↓ α∧␈↓↓␈↓ ¬∧∃l.l ≠ l2 ∧ whither(l1,v,l,␈↓	x␈↓↓)
␈↓ α∧␈↓↓␈↓ ¬T∧ whither(l,u ∪ v,l2,outcome(l1,v,␈↓	x␈↓↓))]]␈↓.


␈↓ α∧␈↓Notice␈αthat␈αthis␈αis␈αa␈αrecursive␈αcharacterization␈αof␈α␈↓↓whither(l1,u ∪ v,l2,␈↓	x␈↓↓)␈↓,␈αsince␈αthe␈αfunction␈αbeing
␈↓ α∧␈↓characterized␈α⊃appears␈α⊃on␈α⊃both␈α⊃sides␈α⊃of␈α⊃the␈α⊃formula.␈α⊃ ␈↓↓outcome(l,u ∪ v,␈↓	x␈↓↓)␈↓␈α⊃is␈α⊃determined␈α⊃by␈α⊂the
␈↓ α∧␈↓relations

␈↓ α∧␈↓␈↓ αT␈↓↓l ε labels(u) ∧ whither(l,u,l2,␈↓	x␈↓↓) ∧ ¬(l2 ε labels(v)) ⊃ outcome(l,u ∪ v,␈↓	x␈↓↓) = outcome(l,u,␈↓	x␈↓↓)␈↓,

␈↓ α∧␈↓␈↓ αT␈↓↓l ε labels(v) ∧ whither(l,v,l2,␈↓	x␈↓↓) ∧ ¬(l2 ε labels(u)) ⊃ outcome(l,u ∪ v,␈↓	x␈↓↓) = outcome(l,v,␈↓	x␈↓↓)␈↓,

␈↓ α∧␈↓␈↓ αT␈↓↓l␈α%ε␈α%labels(u)␈α&∧␈α%whither(l,u,l2,␈↓	x␈↓↓)␈α%∧␈α%l2␈α&ε␈α%labels(v)␈α%⊃␈α&outcome(l,u ∪ v,␈↓	x␈↓↓)␈α%=
␈↓ α∧␈↓↓outcome(l2,u ∪ v,outcome(l,u,␈↓	x␈↓↓))␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓l␈α&ε␈α%labels(v)␈α&∧␈α%whither(l,v,l2,␈↓	x␈↓↓)␈α&∧␈α%l2␈α&ε␈α%labels(u)␈α&⊃␈α&outcome(l,u ∪ v,␈↓	x␈↓↓)␈α%=
␈↓ α∧␈↓↓outcome(l2,u ∪ v,outcome(l,v,␈↓	x␈↓↓))␈↓.

␈↓ α∧␈↓␈↓ αTA␈αtheorem␈αis␈αrequired␈αwhose␈αproof␈αis␈αlikely␈αto␈αbe␈αtedious.␈α Namely,␈α␈↓↓whither(l1,u,l2,␈↓	x␈↓↓)␈↓␈αand
␈↓ α∧␈↓␈↓↓outcome(l,u,␈↓	x␈↓↓)␈↓ do not depend on how the program ␈↓↓u␈↓ is built up from its elementary constituents.